(TML)

let simpth ss :term->thm = snd o (simpterm ss ) ;;

let LISTINDUCT a l p (UUth, NILth, CONSth) =
             %The thms are resp. ]- p[UU/l], ]- p[NIL/l] and
              p ]- p[CONS a l /l] ,  and the result thm will be ]- p .
              We assume that a and l are not free in any hypotheses
              of the arguments thms.
             %
  let UUl,HEADl,TAILl,NULLl = "UU↑l:list","HEAD↑l", "TAIL↑l", "NULL↑l"
  and f = "FFF:list->list"

            %This is a makeshift ; better is
                 mkvar(gentok(), ":list->list")
             to get a completely new variable, since noone will see
             it.
            %
  and SUBlp = SUBST l p
      in
  let w = mkquant(l, substinform(mkcomb(f,l), l, p))

            % w is !l.p[f(l)] . We set up baseth, stepth as
               ]- w[UU/f]  ,  w ]- w[LISTFUN(f)/f]
             respectively, and then use INDUCT to get
               ]- w[FIX(LISTFUN)/f]  -  i.e. ]- !l. p[FIX LISTFUN l] .
             Then ]-p follows by SPEC and LISTAX .
            %

        in
  let baseth = GEN l(SUBlp (SYM(MINAP UUl)) UUth)
  and stepth = GEN l(CASES NULLl CASEths) where CASEths =

            % These will be NULL l == TT/FF/UU ]- p[LISTFUN f l] ;
             first we need three thms :-
             NULL l == TT ]- NIL == LISTFUN f l
             NULL l == FF ]- CONS(HEAD l)(f(TAIL l)) == LISTFUN f l
             NULL l == UU ]- UU == LISTFUN f l
            %

    (let TTeqn, FFeqn, UUeqn =
       (g eqtt, g eqff, g equu  where
       g = \eq. SYM(TRANS(th, simptm
             [BASICSS; (ASSUME(eq NULLl))]
             (rhs(concl th)) ))  where
                 th = APTHM(APTHM defLISTFUN f) l
       )

           % Now we instantiate CONSth for the FF case to get
            w ]- p[CONS(HEAD l)(f (TAIL l))]
           %

      and CONSth = MP
         (INST(HEADl,a)(INST(mkcomb(f,TAILl),l)(DISCH p CONSth)))

            % i.e. p[f(TAIL l)] IMP p[CONS(HEAD l)(f (TAIL l))] %

         (SPEC TAILl (ASSUME w))

            % i.e. w ]- p[f(TAIL l)]  %

       in (SUBlp TTeqn NILth, SUBlp FFeqn CONSth, SUBlp UUeqn UUth)
      )

  in SUBlp (SPEC l LISTAX)
           (SPEC l (INDUCT "LISTFUN" f w (baseth, stepth)) )
;;


let LISTINDUCTAC l (fm,ss,fml) =
  (let a = "A:atom"  in
   [  substinform("UU:list" ,l,fm), ss, fml  ;
      substinform("NIL", l, fm),    ss, fml  ;
      substinform("CONS↑a↑l" ,l,fm), ssadd (ASSUME fm) ss,  fml],
  LISTINDUCT a l fm  o  threeof
  ) ? failwith `LISTINDUCTAC`;;